i, a:Id, T:Type, ds:x:Id fp Type, init:x:Id fp ds(x)?Void, P:(State(ds)TProp).
@i (with ds: ds init: init action a:T precondition a(v) is P s v)  Dsys 

latex

Definitions	Dsys, @i (with ds: ds init: init action a:T precondition a(v) is P s v), if b t else f fi, eqof(d), MsgA, with ds: ds init: initaction a:T precondition a(v) is P, , State(ds), Prop, f(x)?z, IdDeq, a:A fp B(a), x:A. B(x), x. t(x), t  T, Id
Lemmas	Id wf, fpf wf, id-deq wf, fpf-cap wf, ma-state wf, ma-empty wf, ma-single-pre-init wf, msga wf, eqof wf, ifthenelse wf